Extending the Input Language of Spi2Java Seminar: “Selected Topics of Information Security and Cryptography”

Automatic code generation from formal models is an important ap-proach for the secure implementation of cryptographic protocols. We have extended Spi2Java, a tool that automatically generates interoper-able protocols from spi calculus processes to use a more powerful input language. The new input language is the spi calculus with constructors and destructors defined in the paper of Abadi and Blanchet [1]. We have successfully implemented a generic type inference algorithm for the new language constructs and refactored the code significantly. Furthermore, we implemented a translation from the original input language to the spi calculus with constructors and destructors. This paper describes the steps we have taken for implementing this extension, our achievements and remaining work.